Nuprl Definition : f-free
11,40
postcript
pdf
the rcv(free message from
e1
to
j
) == es-first-from(
es
;
e1
;<loc(
e1
),
j
, "$z">;"$free")
latex
clarification:
f-free{$z,$free}(
es
;
e1
;
j
) == es-first-from(
es
;
e1
;<es-loc(
es
;
e1
),
j
, "$z">;"$free")
latex
Definitions
es-first-from(
es
;
e
;
l
;
tg
)
,
loc(
e
)
,
<
a
,
b
>
,
"$x"
FDL editor aliases
f-free
origin